$\forall$$T$:Type, $L_{1}$, $L_{2}$:($T$ List), $x$, $y$:$T$. ($x$ $\in$ $L_{1}$) $\Rightarrow$ ($y$ $\in$ $L_{2}$) $\Rightarrow$ $x$ before $y$ $\in$ $L_{1}$ @ $L_{2}$